Skip to content

Simplify multiple-of-element size access to arrays #8627

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open

Simplify multiple-of-element size access to arrays #8627

wants to merge 2 commits into from

Conversation

tautschnig
Copy link
Collaborator

Array operations may fall back to byte_extract or byte_update expressions in parts of the code base. Simplify this to index or WITH expressions, respectively, when the offset is known to be a multiple of the array-element size.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov Codecov
Copy link

codecov bot commented Apr 14, 2025 •
edited
Loading

Codecov Report

Attention: Patch coverage is 87.62376% with 25 lines in your changes missing coverage. Please review.

Project coverage is 80.40%. Comparing base (0beaf25) to head (3ffb445).

Files with missing lines Patch % Lines
src/util/pointer_offset_size.cpp 81.55% 19 Missing ⚠️
src/util/simplify_expr.cpp 93.93% 6 Missing ⚠️
Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #8627      +/-   ##
===========================================
+ Coverage    80.39%   80.40%   +0.01%     
===========================================
  Files         1688     1688              
  Lines       207129   207316     +187     
  Branches        73       73              
===========================================
+ Hits        166519   166691     +172     
- Misses       40610    40625      +15

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

remi-delmas-3000
remi-delmas-3000 reviewed Apr 14, 2025
View reviewed changes
@remi-delmas-3000
Copy link
Collaborator

Is there a way to share some of the pattern matching conditions between the array-read and array-write cases ?

@remi-delmas-3000
Copy link
Collaborator

Seems like we should also be able to pattern match an access to a member of a struct in an array of structs like a[i].m, the offset would be of the form i*sizeof(T) + offset(T,m) and turn that into a functional update as well ?

@tautschnig tautschnig mentioned this pull request Apr 23, 2025
Open
@tautschnig
Copy link
Collaborator Author

Seems like we should also be able to pattern match an access to a member of a struct in an array of structs like a[i].m, the offset would be of the form i*sizeof(T) + offset(T,m) and turn that into a functional update as well ?

Done.

@tautschnig tautschnig self-assigned this May 30, 2025
@tautschnig tautschnig marked this pull request as draft May 30, 2025 14:13
@tautschnig tautschnig force-pushed the simp_mult_offset branch 2 times, most recently from 65d33b4 to 5c0408c Compare June 3, 2025 11:04
remi-delmas-3000
remi-delmas-3000 reviewed Jun 18, 2025
View reviewed changes
Copy link
Collaborator

@remi-delmas-3000 remi-delmas-3000 left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

From my understanding of the code the cases where we have a symbolic offset value with some shape that does not properly align with the underlying type of the accessed object seem to be handled, but could we add some negative tests for that ?

i.e. tests that check that the array access or array update still reduce to byte-level operations when they are supposed to ?

Also I just thought of the case you mentioned is frequent in the linux kernel, where people access struct fields using a base_pointer + offsetof(T, field), or accessing some array from its end pointer with a negative offset, which I don't think are handled.

@tautschnig tautschnig marked this pull request as ready for review June 24, 2025 13:21
@tautschnig
Tests to demonstrate need for offset pattern matching
1bf65fa 
Although the tests produce correct verification results, the encoding
can be very large as shown in diffblue#8617.
@tautschnig
Simplify multiple-of-element size access to arrays
3ffb445 
Array operations may fall back to byte_extract or byte_update
expressions in parts of the code base. Simplify this to index or WITH
expressions, respectively, when the offset is known to be a multiple of
the array-element size, or a constant offset plus a multiple of the
array-element size.

Fixes: diffblue#8617
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@remi-delmas-3000 remi-delmas-3000 remi-delmas-3000 left review comments

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

At least 1 approving review is required to merge this pull request.

Assignees

@kroening kroening

@peterschrammel peterschrammel

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @remi-delmas-3000 @kroening @peterschrammel